(set-logic QF_NIA)
(declare-const i1 Int)
(declare-const i3 Int)
(declare-const i5 Int)
(check-sat)
(assert (xor true true true true true (xor true (> i1 (* 38 i3 i1)) true true) true true true true))
(assert (> (+ 38 i3 i5 i3) 648))
(push 1)
(assert (= true (<= 0 i3) (= 0 i1 0 (* 38 i3 i1)) true true true))
(assert (< (+ 38 i3 i5 i3) 0))
(check-sat)
(pop 1)
(check-sat)
